$\forall$$A$,$B$:Type, $d$:EqDecider($B$). strong{-}subtype($A$; $B$) $\Rightarrow$ ($d$ $\in$ EqDecider($A$))